#ifndef WRAPPER_H
#define WRAPPER_H


#define pos(var)  (var<<1)
#define neg(var)  ((var<<1)^1)

#define Manager void*

#define sTRUE 1
#define sFALSE 0
#define sUNDEF -1


extern int FF;
extern int TT;	//set in InitManager()

/***********************************************************
 Constructor/DestructorStatusT
 ***********************************************************/
// init a manager
Manager InitManager();

// release a manager
void ReleaseManager(Manager mng);



/***********************************************************
 Problem specification
 ***********************************************************/
// add a variable
int NewVar(Manager mng, int dvar);

// Declare if a variable should be eligible for selection in the decision heuristic.
void SetDecisionVar(Manager mng, int var, int b);

// add a clause
void AddClause(Manager mng, int num_lits, int* clause_lits);



/***********************************************************
 Solving
 ***********************************************************/
//solve
int Solve(Manager mng);

int GetVar(Manager mng, int var);
int GetVarInt(Manager mng, int size, int* vars);
void dump_vars(Manager mng);
/***********************************************************
 Read state
 ***********************************************************/
// The current number of original clauses.
int NumClauses(Manager mng);

// The current number of variables.
int NumVars(Manager mng);


/*============================================================
 ============================================================*/
typedef void (*GATE) (Manager mng, int size, int o, int* a);

int* NewVarS(Manager mng, int size, int dvar);

int* NewVarGate(Manager mng, int size, int dvar, GATE gate, int predef_size, int o, ...);

int* int2bools(Manager mng, int size, int c);


void BeginAssumption(Manager mng);
void Assume(Manager mng, int o);
void AssumeNot(Manager mng, int o);
void EndAssumption(Manager mng);

void Assert(Manager mng, int o);

void AssertNot(Manager mng, int o);

void Imply(Manager mng, int a, int b);

void ImplyNot(Manager mng, int a, int b);

void Or2(Manager mng, int o, int a, int b);

void Or3(Manager mng, int o, int a, int b, int c);

void Or(Manager mng, int size, int o, int* a);

void And2(Manager mng, int o, int a, int b);

void And3(Manager mng, int o, int a, int b, int c);

void And(Manager mng, int size, int o, int* a);

void Xor(Manager mng, int o, int a, int b);
void XNor(Manager mng, int o, int a, int b);

void Eq(Manager mng, int size, int o, int* a, int* b);

void Eq_const(Manager mng, int size, int o, int* a, int c);

void Neq(Manager mng, int size, int o, int* a, int* b);

void Neq_const(Manager mng, int size, int o, int* a, int c);

void Lt(Manager mng, int size, int o, int* a, int* b);

void Leq(Manager mng, int size, int o, int* a, int* b);

//o = (res=a+c)
void Sum_const(Manager mng, int size, int o, int* res, int* a, int c);

//o = a /\ (b\/c) 
void a_And_b_Or_c(Manager mng, int o, int a, int b, int c);
#endif










